$\forall$$i$, $a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}$). Dec($\exists$$v$:$T$. $P$($s$,$v$)))
\\[0ex]$\Rightarrow$ @$i$ precondition for $a$(v:$T$):$P$ State(${\it ds}$) v $\Vdash$ ${\it es}$.@$i$ Precondition for $a$(v)$P$ State(${\it ds}$) (v:$T$)